(set-logic ALL)
(set-info :status sat)
(declare-sort g 0)
(declare-fun g (g) Int)
(declare-fun r () Int)
(declare-fun c () Int)
(declare-fun i () Int)
(declare-fun o () (_ BitVec 1))
(declare-fun o1 () (_ BitVec 1))
(declare-fun o2 () g)
(assert (= (g o2) (ite (< 0 (+ (bv2nat o1) (bv2nat o))) (+ (bv2nat o1) (bv2nat o1)) 0)))
(check-sat)
